-- -*-Haskell-*-

{-
 * Copyright (c) 2007-2008 Gabor Greif
 *
 * Permission is hereby granted, free of charge, to any person obtaining a copy
 * of this software and associated documentation files (the "Software"), to deal
 * in the Software without restriction, including without limitation the rights
 * to use, copy, modify, merge, publish, distribute, sublicense, and/or sell copies
 * of the Software, and to permit persons to whom the Software is furnished to do
 * so, subject to the following conditions:
 *
 * The above copyright notice and this permission notice shall be
 * included in all copies or substantial portions of the Software.
 *
 * THE SOFTWARE IS PROVIDED "AS IS", WITHOUT WARRANTY OF ANY KIND,
 * EXPRESS OR IMPLIED, INCLUDING BUT NOT LIMITED TO THE WARRANTIES
 * OF MERCHANTABILITY, FITNESS FOR A PARTICULAR PURPOSE AND
 * NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS OR COPYRIGHT
 * HOLDERS BE LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY,
 * WHETHER IN AN ACTION OF CONTRACT, TORT OR OTHERWISE, ARISING
 * FROM, OUT OF OR IN CONNECTION WITH THE SOFTWARE OR THE USE
 * OR OTHER DEALINGS IN THE SOFTWARE.
 -}

-- Usage:
--
--  Set up the environment
--     setenv LD_LIBRARY_PATH /opt/exp/gnu/lib:$LD_LIBRARY_PATH
--     setenv PATH /home/ggreif/%NoBackup%/Omega1.4.2:$PATH
--
--  Start the omega interpreter by typing
--     omega Thrist.omg
--  and run your commands on the prompt
--

import "LangPrelude.prg" 
  (head,tail,lookup,member,fst,snd,map,Monad,maybeM,id,ioM,Row,RCons,RNil,Eq,Equal,
  listM, (!=), (==))

kind Doe = Wi | So

data DooBiDoo :: Doe ~> Doe ~> *0 where
  ToWi :: DooBiDoo a Wi
  SoToWi :: DooBiDoo So Wi
  WiToWi :: DooBiDoo Wi Wi
  WiToSo :: DooBiDoo Wi So
  SoTo :: DooBiDoo So b
  ToSo :: DooBiDoo a So

data ShuBiDoo :: Doe ~> Doe ~> *0 where
  WiTo :: ShuBiDoo Wi a

--$   @Definition { A @I thrist is a list-like datastructure
--$ with three type indices. It enforces the invariants that
--$ @List { @Item { it can only contain members of the same type with two type indices
--$ and } @Item { that the type indices of consequtive members must match
--$ up in the specific manner that the second type index of the
--$ left member must equal the first type index of the right one. } } }

--{
data Thrist :: forall (l :: *1) . (l ~> l ~> *)  ~> l ~> l ~> * where
  Nil :: Thrist k a a
  Cons :: k a b -> Thrist k b c -> Thrist k a c
 deriving List(l)
--}

--$   @Note { The name thrist is a portmanteau of thread and list
--$ conveying the essence of a list where the members' types are
--$ threaded up. }

{--@
By means of the @Code { deriving List(l) } declaration
we specified that thrists can be entered in @Omega using
special syntax, making it amenable to reading from the
listener, pattern matching and outputting.
@P The following example session demonstrates this:
--@-}

{- Example session:

prompt> []l
 []l : forall (a:*1) (b:a ~> a ~> *0) (c:a:*1).Thrist b c c
prompt> [ToWi]l
 [ToWi]l : forall (a:Doe).Thrist DooBiDoo a Wi
prompt> [ToWi,WiToWi]l
 [ToWi,WiToWi]l : forall (a:Doe).Thrist DooBiDoo a Wi
prompt> [ToWi,WiToWi,ToSo]l
 [ToWi,WiToWi,ToSo]l : forall (a:Doe).Thrist DooBiDoo a So
prompt> [ToWi,WiToWi,ToSo,SoTo]l
 [ToWi,WiToWi,ToSo,SoTo]l : forall (a:Doe) (b:Doe).Thrist DooBiDoo a b
prompt> [ToWi, WiTo]l
 In the expression: Cons WiTo Nil
 the result type: Thrist ShuBiDoo Wi b
 was not what was expected: Thrist DooBiDoo Wi a

-}

##test "different constants: ShubiDoo   !=   DooBiDoo"
 fail0 = [ToWi, WiTo]l

cat :: Thrist DooBiDoo a b -> String
cat Nil = ""
cat (Cons ToWi r) = "ToWi " ++ cat r
cat (Cons WiToWi r) = "WiToWi " ++ cat r
cat (Cons WiToSo r) = "WiToSo " ++ cat r
cat (Cons SoTo r) = "SoTo " ++ cat r
cat (Cons ToSo r) = "ToSo " ++ cat r

runThrist :: forall (a :: *0~>*0~>*0) . (forall (b :: *0).a b b)
	     -> (forall (b :: *0) (c :: *0) (d :: *0).a b c -> a c d -> a b d)
	     -> Thrist a b c
	     -> a b c
runThrist n _ []l = n
runThrist n c [h; t]l = c h (runThrist n c t)



------------------------------------
-- representing polynomial datatypes
------------------------------------
{- does not work yet
how :: *0 ~> Prod *0
{how (t -> u)} = PCons t {how u}
{how Int} = PCons Int PNil
{how Bool} = PCons Bool PNil

last :: *0 ~> Prod *0
{last (t -> u)} = {last u}
{last Int} = Int
{last Bool} = Bool



data Sum :: *0 ~> Prod *0 ~> *0 where
  Fin :: Sum a PNil
  Case :: t -> Sum a b -> Sum a {how t}
 deriving List(s)

--tp1 :: Sum Bool (Prod a)
tp0 = [False, True]s
tp1 = [Nothing, Just]s
-}

##test "Mixup in Decs (not reported yet)"
 Weee :: Prod *0
 type Weee = PNil



--$ @Section { Crazy uses of Thrists }
--$ For example we can put functions of type
--$ a->b, b->c into a thrist:

--{
funThrist = [ord, (+) 2, chr]l

runArrThrist :: Thrist (->) a b -> a -> b
runArrThrist Nil b = b
runArrThrist (Cons f r) a = runArrThrist r (f a)
--}

{-
-- Example session:

prompt> funThrist
 [<primfun to1>,<fn>,<primfun to1>]l : Thrist (->) Char Char
prompt> runArrThrist funThrist
 <fn> : Char -> Char
prompt> runArrThrist funThrist 'x'
 'z' : Char

-}


-- Thrist (,)

{-
-- Example session:
prompt> [(1, 'h'), ('u', "ss")]l
 [(1,'h'),('u',"ss")]l : Thrist (,) Int [Char]
-}

-- Thrist (+)

-- Thrist Bind
{-
-- Example session:
prompt> [fuse 2 ""]l
TODO###
-}

-- Thrist ContM

-- Thrist EqTag

-- Thrist (!=)

-- Thrist (==) -- NOT COMPATIBLE

--$ @Item { An interesting use are @Code { Equal } thrists
--$ as they can express transitivity relationships of
--$ type equality: @Code { Equal a b /\ Equal b c ==> Equal c a }

plus:: Nat ~> Nat ~> Nat
{plus Z m} = m
{plus (S n) m} = S {plus n m}

plusZ :: Nat' n -> Equal {plus n Z} n
plusZ Z = Eq
plusZ (S n) = Eq -- :: Equal {plus (S n) Z} (S n) -- reduces to Equal (S {plus n Z}) (S n)
  where theorem because = plusZ n -- :: Equal {plus n Z} n


plusS :: Nat' n -> Equal {plus n (S m)} (S {plus n m})
plusS Z = Eq :: Equal {plus Z (S m)} (S {plus Z m}) --> Equal (S m) (S {plus Z m}) --> Equal m {plus Z m} --> Equal m m
plusS (S n) = Eq --::  Equal {plus (S n) (S m)} (S {plus (S n) m})
                   --> Equal (S {plus n (S m)}) (S (S {plus n m}))
                   --% Equal    {plus n (S m)}     (S {plus n m})
    where theorem because = plusS n


plusCommutes :: Nat' n -> Nat' m -> Equal {plus n m} {plus m n}
plusCommutes Z m = Eq --:: Equal {plus Z m} {plus m Z}
                      -->  Equal m {plus m Z}
    where theorem because = plusZ m

plusCommutes (S n) m = Eq --:: Equal {plus (S n) m} {plus m (S n)}
                          -->  Equal (S {plus n m}) {plus m (S n)}
                          --%  Equal (S {plus n m}) (S {plus m n})
                          --%  Equal    {plus n m}     {plus m n}
    where theorem because1 = plusS m, because2 = plusCommutes n m

impliesZero :: Nat' n -> Nat' m -> Equal {plus n m} m -> Equal m Z

{-
##test "current refinement fails because _a != {plus 0t _a}"
 impliesZero Z m Eq = Eq --? Equal {plus Z m} m -> Equal m Z
                        --> Equal m m -> Equal m Z
-}
{-
##test "Annotation not polymorphic enough"
 impliesZero Z (m :: Nat' m')  (Eq :: Equal m' m') = Eq --? Equal {plus Z m} m -> Equal m Z
                        --> Equal m m -> Equal m Z
-}
impliesZero (S n) m Eq = unreachable --? Equal {plus (S n) m} m -> Equal m Z
                                     --> Equal (S {plus n m}) m -> Equal m Z

{-
impliesZero (S n) Z Eq = unreachable --? Equal {plus (S n) Z} Z -> Equal Z Z
                                     --> Equal (S {plus n Z}) Z -> Equal Z Z
                                     --% Equal (S n) Z -> Equal Z Z
--    where theorem plusZ


impliesZero (S n) (S m) Eq = unreachable --? Equal {plus (S n) (S m)} (S m) -> Equal (S m) Z
                                      --> Equal (S {plus n m}) m -> Equal m Z
-}




--$ I am writing this as an equivalent thrist now


{-
hyp1 :: Nat' a -> Nat' (S b) -> Equal a (S b)
hyp1 #1 #1 = Eq
hyp1 (S a) (S b) = Eq
  where theorem because = hyp1 a b
-}

##test "Does not work yet"
 eqThrist = [Eq :: Equal a (S b)
            , Eq :: Equal (S b) (S c)
            , Eq :: (S c) a
            ]l
